Code and Notes (Week 9 Wednesday)

{-# LANGUAGE DataKinds, KindSignatures #-}
-- ^ language pragma: describes the set of language extensions enabled
-- in this file
module W9A where

{- Thought experiment:
   Suppose a Haskell function has type

       foo :: Int -> Int

   When type-checking the function foo,
   Haskell's type inferencer proves
   a theorem for you!

   And the theorem is:
   - if you give foo an argument x of
     type Int,
     foo will *not* return output of
     any type other than Int.

   Note: I didn't say:
     "foo will return output of type Int"
   ..because type judgements do not
     guarantee totality of functions.

   When we prove (using induction and equational reasoning)
   that

     map (f . g) xs = map f (map g xs)

   ^ we *know* that this works for every possible execution
     of the above program(s)

   Similary, the guarantee from the type system
   (that foo never returns types other than Int)
   hold for every possible execution.
 -}

{- The halting problem:

     Can we write a program P that,
       given the source code of an arbitrary program Q,
     - be total (always successfully terminate)
     - return true iff execution of Q would halt (terminate)

   This is impossible (there is no such P).

   Suppose we have such a program:  halt(Q) returns true if Q halts,
                                                    false otherwise.

   then build the following program:

    bool nonsense() {
      if halt(nonsense()) then
        while true do skip;
      else return true
    }

    ^ this program terminates iff it doesn't


  Undecidable: there is no (total) algorithm that
   always gives a correct solution to the problem

  A *trivial* property is either:
  - true for all possible inputs, or
  - false for all possible inputs
 -}

my_prop :: Int -> Bool
my_prop n = True -- trivial

my_prop2 :: Int -> Bool
my_prop2 n = even n -- non-trivial

{-
  Semantic properties:

   - The program never returns 5 for any input
   - The program always returns at least 36

  Syntactic properties:

   - The program contains an if/then/else statement
   - The program doesn't contain a `while` loop

  Static checkers usually *don't* directle analyse semantic properties.
  Instead, they *approximate* semantic properties using syntactic properties.


  For example (A),
    instead of check directly "does the program terminate?"

  We can check (B):
    does the program contain any recursion or loops?

  There will be some programs that contain recursion and loops,
    and still terminate.

  But: we know that B implies A.

  Any static check is therefore by necessity going to rule out
  some perfectly fine programs.


fake_haskell :: Int
fake_haskell =
 let xs = [1,2,"hello"] -- this will not type check
 in hd xs -- ...but we nonetheless know  that we'll always get an Int back

When the type system proves fake_haskell :: Int

 - It isn't checking the semantic property "is the value of fake_haskell of type Int?"
 - It is checking a syntactic property

 -}


-- Problem: given an Double, we don't know its unit of measure
-- Can we get the type system to prevent unit of measure confusion?

-- First solution: distinct datatypes for kilometers and miles

data Kilometer = Kilometer Double deriving (Eq,Show)
data MMile = MMile Double deriving (Eq,Show)

addKm :: Kilometer -> Kilometer -> Kilometer
addKm (Kilometer x) (Kilometer y) = Kilometer(x+y)

addMMile :: MMile -> MMile -> MMile
addMMile (MMile x) (MMile y) = MMile(x+y)

{- This definitely prevents the type confusion!

   But: now we have redefine all of arithmetic
        again for every possible unit
 -}

-- Phantom types
{- Encode the unit as a *type parameter*
   rather than a distinct type
 -}
data Distance a = Distance Double deriving (Eq,Show)
-- I've written a datatype declaration that
-- takes a type argument but doesn't use it
-- This type argument is a phantom type

-- These types have *no* data constructors (and therefore no values inhabit hem)
-- these are only intended to used to instantiate phantom types
data Km
data Mile
data Square a

km5 :: Distance Km
km5 = Distance 5

mile5 :: Distance Mile
mile5 = Distance 5

add :: Distance a -> Distance a -> Distance a
add (Distance x) (Distance y) = Distance(x+y)

times :: Distance a -> Distance a -> Distance(Square a)
times (Distance x) (Distance y) = Distance(x*y)

data Student l = Student String deriving (Eq,Show)

type ZID = Int

-- takes a type argument but doesn't use it
-- This type argument is a phantom type

-- These types have *no* data constructors (and therefore no values inhabit hem)
-- these are only intended to used to instantiate phantom types
data UG
data PG

--data Student l = Student String deriving (Eq,Show)

getName :: Student l -> String
getName(Student name) = name

enrollInCOMP3161 :: Student UG -> IO()
enrollInCOMP3161 s =
  putStrLn $ "Enrolled in COMP3161: " ++ getName s

enrollInCOMP9164 :: Student PG -> IO()
enrollInCOMP9164 s =
  putStrLn $ "Enrolled in COMP9164: " ++ getName s

studentDB :: ZID -> Either (Student PG) (Student UG)
studentDB 0 = Left(Student "Jean-Baptiste Bernadotte")
studentDB 1 = Right(Student "Hrafna-Flóki Vilgerðarson")
studentDB n = Right(Student "<UNKNOWN STUDENT>")

enroller :: IO ()
enroller = do
  putStrLn "Give me a zID:"
  zid <- readLn
  case studentDB zid of
    Left student ->
      enrollInCOMP9164 student
    Right student ->
      enrollInCOMP3161 student
  enroller

{- There's one annoying thing here:
   - once we've put the UG/PG distinguisher into the types,
   - *every* function that returns a student now needs this
         Either (Student UG) (Student PG)
     construction
 -}

{- Haskell doesn't let us do the same thing (out of the box)
       Sq<X extends Unit>

   The type system of Haskell is (almost) untyped.

   Types have kinds

     Int    :: *
     Bool   :: *
     [Bool] :: *

     Maybe  :: * -> *
     IO     :: * -> *

   ...when you have a type variable such as a phantom type,
      unless otherwise specified, it can be instantiated
      to anything of kind *.

   There is a simple language extension to make the
   type system more typed.
   It allows us to introduce our own kinds,
   in addition to *, * -> *  ...

   KindSignatures:
    --- allows type variables to be annotated with their kind
 -}
--data MyType (a :: (* -> *)) = MyType

{- DataKinds:
   - extends datatypes so that they define *two things*
      - a type, and the values that inhabit it
      - a kind, and the types that inhabit it
 -}
data Nat = Z | Suc Nat
{- Without DataKinds, this defines:
   a type Nat
   two values
      Z :: Nat
      Suc :: Nat -> Nat

   With DataKinds, it also defines:
   a *kind* called Nat (distinct from *)
   two types that inhabit our kind
      Z :: Nat
      Suc :: Nat -> Nat
 -}

data Unit = KmU | MileU | SquareU Unit

data DistanceU (a :: Unit) = DistanceU Double deriving (Eq,Show)

km5U :: DistanceU KmU
km5U = DistanceU 5.0

--b5U :: DistanceU Bool
--b5U = DistanceU 5.0

{- The *kind* Nat,
   contains types Z, Suc(Z) and so on

   .. but these types contain no values
 -}

{- - Make illegal states unrepresentable
   - Parse, don't validate
   ^ The techniques showed here help you do both.

   But there's still a lot you can do without phantom types
 -}

-- Soccer (aka football) play-by-blay

data Matildas = SamKerr | MaryFowler deriving (Eq,Show)

data Sweden = FridolinaRolfö | KosovaraAsllani deriving (Eq,Show)

{- A play-by-play where team a controls the ball
 -}
data Match a b = 
  Goal a (Match a b)
  | Kickoff a
  | Pass a (Match a b)
  | Steal a (Match b a)
  deriving (Eq,Show)

myMatch :: Match Matildas Sweden
myMatch =
  Steal MaryFowler $ Pass MaryFowler $ Kickoff SamKerr
--  Pass MaryFowler
--  $
--  Steal FridolinaRolfö
--  $
--  Pass MaryFowler
--  $
--  Kickoff SamKerr

class Unit {}

class Km extends Unit {}
class Mile extends Unit {}
class Sq<X extends Unit> extends Unit {}

class Distance<X extends Unit> {
    Distance(int distance) {
        this.distance = distance;
    }

    private int distance;

    public Distance<X> add(Distance<X> dist) {
        return new Distance<X>(distance + dist.distance);
    }

    public Distance<Sq<X>> times(Distance<X> dist) {
        return new Distance<Sq<X>>(distance * dist.distance);
    }
}

public class Units {

    public static void main(String[] args) {
        Distance<Km> km5 = new Distance<Km>(5);
        Distance<Mile> mile5 = new Distance<Mile>(5);

        km5.add(mile5); // this will not compile!
    }
}